nLab typal equality

 Idea

In dependent type theory, the term typal equality is used to describe the use of the identity type to represent the notion of equality of terms, and is primarily used to distinguish from the notion of judgmental equality of terms.

In dependent type theories with a separate proposition judgment $\phi \mathrm{prop}$, the term typal equality is also used to distinguish identity types from propositional equality, which is the equality judged to be a proposition; i.e. $a =_A b \mathrm{prop}$. On the other hand, in dependent type theory without a separate proposition judgment, propositions are usually defined to be certain types, and the term “propositional equality” is used as a synonym of typal equality in referring to identity types. (In fact, “propositional equality” is the older and arguably still more common term in this context.)

 See also

• judgmental equality of terms
• propositional equality